/*
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * 
 * This file is part of SYMBOLRT.
 *
 * SYMBOLRT is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * SYMBOLRT is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with SYMBOLRT.  If not, see <http://www.gnu.org/licenses/>.
 *
 *
 * REVISION HISTORY:
 * Author                           Date           Brief Description
 * -------------------------------- -------------- ------------------------------
 * Wilkerson de Lucena Andrade      19/04/2012     Initial version
 * 
 */
package br.edu.ufcg.symbolrt.main;

import java.util.List;

import br.edu.ufcg.symbolrt.algorithms.ParallelComposition;
import br.edu.ufcg.symbolrt.algorithms.SequentialComposition;
import br.edu.ufcg.symbolrt.algorithms.SynchronousProduct;
import br.edu.ufcg.symbolrt.algorithms.TestPurposeCompletion;
import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.examples.Radar;
import br.edu.ufcg.symbolrt.examples.TargetDesignation;
import br.edu.ufcg.symbolrt.examples.TargetTracking;
import br.edu.ufcg.symbolrt.exception.ClockGuardException;
import br.edu.ufcg.symbolrt.exception.IncompatibleSynchronousProductException;
import br.edu.ufcg.symbolrt.symbolicexecution.exception.IncompatibleOperationException;
import br.edu.ufcg.symbolrt.symbolicexecution.algorithms.SymbolicExecution;
import br.edu.ufcg.symbolrt.symbolicexecution.algorithms.TestCaseSelection;
import br.edu.ufcg.symbolrt.symbolicexecution.algorithms.TestTreeTransformation;
import br.edu.ufcg.symbolrt.symbolicexecution.base.SymbolicExecutionTree;
import br.edu.ufcg.symbolrt.symbolicexecution.base.SymbolicState;
import br.edu.ufcg.symbolrt.symbolicexecution.base.SymbolicTransition;
import br.edu.ufcg.symbolrt.symbolicexecution.exception.SymbolicValueNameException;
import br.edu.ufcg.symbolrt.util.Constants;
import br.edu.ufcg.symbolrt.util.GraphVisualization;


/**
 * <code>Main</code> Class. <br>
 * This class contains the main for executing the SYMBOLRT tool.
 * 
 * @author Wilkerson de Lucena Andrade  ( <a href="mailto:wilkerson@computacao.ufcg.edu.br">wilkerson@computacao.ufcg.edu.br</a> )
 * 
 * @version 1.0
 * <br>
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * <br>
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * <br>
 * <a href="https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt">https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt</a>
 */
public class MainCaseStudySequential {
	
	   public static void main(String[] args) {
		   
		   long startTime = System.currentTimeMillis();
	    	
	        GraphVisualization tiostsVis = new GraphVisualization();
	        
	        TIOSTS spec = generateComposition();
	        tiostsVis.save(spec);
	        
	        TIOSTS tp = createTestPurpose();
	        tiostsVis.save(tp);
	        
	        TestPurposeCompletion completionOperation = TestPurposeCompletion.getInstance();
	        TIOSTS tpComplete = null;
	        try {
	                tpComplete = completionOperation.complete(tp);
	        } catch (ClockGuardException e) {
	                System.out.println(e.getMessage());
	        }
	        tiostsVis.save(tpComplete);
	        
	        SynchronousProduct synchronousOperation = SynchronousProduct.getInstance();
	        TIOSTS sp = null;
	        try {
	                sp = synchronousOperation.synchronousProduct(spec, tpComplete);
	        } catch (IncompatibleSynchronousProductException e) {
				// TODO Auto-generated catch block
				e.printStackTrace();
			}
	        tiostsVis.save(sp);
	        
	        // *********************** Symbolic Execution *********************** 
	        SymbolicExecution symb = SymbolicExecution.getInstance();
	        SymbolicExecutionTree zset = null;
	        try {
	                zset = symb.execute(sp);
	        } catch (SymbolicValueNameException e) {
	                System.out.println(e.getMessage());
	        }
	        
	        // *********************** Test Case Selection ***********************
	        TestCaseSelection tc = TestCaseSelection.getInstance();
	        List<SymbolicExecutionTree> testCases = tc.selectAllTestCases(zset);
	        
	        System.out.println("Number of TCs: " + testCases.size());
	        //printZSET(testCases.get(0));
	        
	        
	        // *********************** Test Tree Transformation ***********************
	        //TestTreeTransformation tt = TestTreeTransformation.getInstance();
	        //TIOSTS testCase = tt.translateTestTree(testCases.get(0), sp);
	        
	        //tiostsVis.save(testCase);
	        
	        for(int i = 0; i < testCases.size(); i++){
	        	printZSET(testCases.get(i));
	            // *********************** Test Tree Transformation ***********************
	            TestTreeTransformation tt = TestTreeTransformation.getInstance();
	            TIOSTS testCase = tt.translateTestTree(testCases.get(i), sp);
	            testCase.setName("testCase" + i);            
	            tiostsVis.save(testCase);
	        }
	        
	        long endTime = System.currentTimeMillis();
	        long totalTime = endTime - startTime;
	        System.out.println("Time spent: "+totalTime);
	}
	    
	    public static TIOSTS generateComposition(){
			/*Composicao do sistema
			 * ((TD;TT)||Radar)
			 */

			TIOSTS tiostsTD = TargetDesignation.createSPEC();
			TIOSTS tiostsTT = TargetTracking.createSPEC();
			TIOSTS tiostsRadar = Radar.createSPEC();

			SequentialComposition seqComposition = SequentialComposition.getInstance();
			ParallelComposition parComposition = ParallelComposition.getInstance();
			TIOSTS sequentialTarget=null, parallelTargetRadar = null;
			GraphVisualization visualization = new GraphVisualization();

			try {
			sequentialTarget = seqComposition.sequentialComposition(tiostsTD, tiostsTT);
			parallelTargetRadar = parComposition.parallelComposition(sequentialTarget, tiostsRadar);
			
			visualization.save(sequentialTarget);

			}catch (IncompatibleOperationException e) {
				e.printStackTrace();
			} 

			return sequentialTarget;   
	    }
		
	    public static void printZSET(SymbolicExecutionTree zset) {
	        System.out.println("*********************** States ***********************");
	        for (SymbolicState zses : zset.getSymbolicStates()) {
	                System.out.println(zses.toString() + "\n\n");
	        }
	        
	        System.out.println("*********************** Transitions ***********************");
	        for (SymbolicState zses : zset.getSymbolicStates()) {
	                for (SymbolicTransition t : zses.getChildrenTransitions()) {
	                        System.out.println(t.toString() + "\n");
	                }
	        }
	}
		
	    public static TIOSTS createTestPurpose(){
	        TIOSTS tiosts = new TIOSTS("TP");
	        
	        //Parameters
	        TypedData op = new TypedData("op", Constants.TYPE_INTEGER);
	        tiosts.addActionParameter(op);

	        // Input, output, and internal actions
	        Action init = new Action("init1", Constants.ACTION_INTERNAL);
	        tiosts.addAction(init);
	         
	        Action finishTargetDesignation = new Action("finishTargetDesignation", Constants.ACTION_OUTPUT);
	        finishTargetDesignation.addParameter(op.getName());
	        tiosts.addAction(finishTargetDesignation);
	        
	        // Locations
	        Location start = new Location("START");
	        tiosts.addLocation(start);
	        Location accept = new Location(Constants.VERDICT_ACCEPT);
	        tiosts.addLocation(accept); 
	        Location s6 = new Location("S60");
	        tiosts.addLocation(s6);
	        
	        // Initial Condition
	        tiosts.setInitialCondition(Constants.GUARD_TRUE);
	        
	        // Initial Location
	        tiosts.setInitialLocation(start);

	        // Transitions
	        tiosts.createTransition("START", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S60");
	        tiosts.createTransition("S60", Constants.GUARD_TRUE, Constants.GUARD_TRUE, finishTargetDesignation, null, null, Constants.VERDICT_ACCEPT);
	        
	        return tiosts;
	}
	    
}
